<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
            "http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML>
<HEAD>

<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<META name="GENERATOR" content="hevea 1.09">
<LINK rel="stylesheet" type="text/css" href="Reference-Manual.css">
<TITLE>Global Index</TITLE>
</HEAD>
<BODY >
<A HREF="biblio.html"><IMG SRC="previous_motif.gif" ALT="Previous"></A>
<A HREF="toc.html"><IMG SRC="contents_motif.gif" ALT="Up"></A>
<A HREF="tactic-index.html"><IMG SRC="next_motif.gif" ALT="Next"></A>
<HR>
<H1 CLASS="chapter">Global Index</H1><P></P><TABLE CELLSPACING=6 CELLPADDING=0><TR><TD VALIGN=top ALIGN=left><UL CLASS="indexenv"><LI CLASS="li-indexenv">
<TT>&#X2223;&#X2223;</TT>, <A HREF="Reference-Manual011.html#@default628">9.2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>*</TT>, <A HREF="Reference-Manual005.html#@default186">3.1.3</A>, <A HREF="Reference-Manual005.html#@default261">3.2.2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>+</TT>, <A HREF="Reference-Manual005.html#@default181">3.1.3</A>, <A HREF="Reference-Manual005.html#@default260">3.2.2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>-</TT>, <A HREF="Reference-Manual005.html#@default262">3.2.2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>/</TT>, <A HREF="Reference-Manual005.html#@default263">3.2.2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">2-level approach, <A HREF="Reference-Manual010.html#@default575">8.10.4</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>;</TT>, <A HREF="Reference-Manual011.html#@default617">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>;[&#X2026;</TT><TT>&#X2223;</TT><TT>&#X2026;</TT><TT>&#X2223;</TT><TT>&#X2026;]</TT>, <A HREF="Reference-Manual011.html#@default619">9.2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>&lt;</TT>, <A HREF="Reference-Manual005.html#@default266">3.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>&lt;=</TT>, <A HREF="Reference-Manual005.html#@default264">3.2.2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>&gt;</TT>, <A HREF="Reference-Manual005.html#@default267">3.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>&gt;=</TT>, <A HREF="Reference-Manual005.html#@default265">3.2.2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>?</TT>, <A HREF="Reference-Manual010.html#@default445">8.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>?=</TT>, <A HREF="Reference-Manual005.html#@default268">3.2.2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">%, <A HREF="Reference-Manual013.html#@default697">11.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>&amp;</TT>, <A HREF="Reference-Manual005.html#@default197">3.1.4</A>
</LI><LI CLASS="li-indexenv">_, <A HREF="Reference-Manual003.html#@default25">1.2.11</A>
</LI><LI CLASS="li-indexenv"><TT>{A}+{B}</TT>, <A HREF="Reference-Manual005.html#@default207">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>{x:A &amp; (P x)}</TT>, <A HREF="Reference-Manual005.html#@default196">3.1.4</A>
</LI><LI CLASS="li-indexenv">{x:A | (P x)}, <A HREF="Reference-Manual005.html#@default190">3.1.4</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">|, <A HREF="Reference-Manual005.html#@default191">3.1.4</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>A*B</TT>, <A HREF="Reference-Manual005.html#@default185">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>A+{B}</TT>, <A HREF="Reference-Manual005.html#@default211">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>A+B</TT>, <A HREF="Reference-Manual005.html#@default180">3.1.3</A>
</LI><LI CLASS="li-indexenv">Abbreviations, <A HREF="Reference-Manual013.html#@default702">11.3</A>
</LI><LI CLASS="li-indexenv"><TT>Abort</TT>, <A HREF="Reference-Manual009.html#@default419">7.1.6</A>
</LI><LI CLASS="li-indexenv"><TT>About</TT>, <A HREF="Reference-Manual008.html#@default340">2</A>
</LI><LI CLASS="li-indexenv">Absolute names, <A HREF="Reference-Manual004.html#@default105">2.6.2</A>
</LI><LI CLASS="li-indexenv"><TT>Acc</TT>, <A HREF="Reference-Manual005.html#@default248">3.1.6</A>
</LI><LI CLASS="li-indexenv"><TT>Acc_inv</TT>, <A HREF="Reference-Manual005.html#@default249">3.1.6</A>
</LI><LI CLASS="li-indexenv"><TT>Acc_rec</TT>, <A HREF="Reference-Manual005.html#@default250">3.1.6</A>
</LI><LI CLASS="li-indexenv"><TT>Add Field</TT>, <A HREF="Reference-Manual010.html#@default597">8.12.10</A>, <A HREF="Reference-Manual025.html#@default789">20.8</A>
</LI><LI CLASS="li-indexenv"><TT>Add Legacy Abstract Ring</TT>, <A HREF="Reference-Manual025.html#@default795">2</A>
</LI><LI CLASS="li-indexenv"><TT>Add Legacy Abstract Semi Ring</TT>, <A HREF="Reference-Manual025.html#@default796">3</A>
</LI><LI CLASS="li-indexenv"><TT>Add Legacy Field</TT>, <A HREF="Reference-Manual025.html#@default798">20.9.4</A>
</LI><LI CLASS="li-indexenv"><TT>Add Legacy Ring</TT>, <A HREF="Reference-Manual025.html#@default791">20.9.1</A>, <A HREF="Reference-Manual025.html#@default793">20.9.2</A>
</LI><LI CLASS="li-indexenv"><TT>Add Legacy Semi
Ring</TT>, <A HREF="Reference-Manual025.html#@default794">1</A>
</LI><LI CLASS="li-indexenv"><TT>Add Legacy Semi Ring</TT>, <A HREF="Reference-Manual025.html#@default792">20.9.1</A>
</LI><LI CLASS="li-indexenv"><TT>Add LoadPath</TT>, <A HREF="Reference-Manual008.html#@default374">6.5.3</A>
</LI><LI CLASS="li-indexenv"><TT>Add ML Path</TT>, <A HREF="Reference-Manual008.html#@default378">6.5.7</A>
</LI><LI CLASS="li-indexenv"><TT>Add Morphism</TT>, <A HREF="Reference-Manual026.html#@default801">21.2</A>, <A HREF="Reference-Manual026.html#@default809">21.9</A>
</LI><LI CLASS="li-indexenv"><TT>Add Printing If </TT><I><FONT COLOR=maroon>ident</FONT></I>, <A HREF="Reference-Manual004.html#@default83">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Add Printing Let </TT><I><FONT COLOR=maroon>ident</FONT></I>, <A HREF="Reference-Manual004.html#@default79">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Add Rec LoadPath</TT>, <A HREF="Reference-Manual008.html#@default375">6.5.4</A>
</LI><LI CLASS="li-indexenv"><TT>Add Rec ML Path</TT>, <A HREF="Reference-Manual008.html#@default379">6.5.8</A>
</LI><LI CLASS="li-indexenv"><TT>Add Relation</TT>, <A HREF="Reference-Manual026.html#@default800">21.2</A>
</LI><LI CLASS="li-indexenv"><TT>Add Ring</TT>, <A HREF="Reference-Manual010.html#@default593">8.12.9</A>, <A HREF="Reference-Manual025.html#@default785">20.5</A>
</LI><LI CLASS="li-indexenv"><TT>Add Setoid</TT>, <A HREF="Reference-Manual026.html#@default808">21.9</A>
</LI><LI CLASS="li-indexenv"><TT>Admitted</TT>, <A HREF="Reference-Manual003.html#@default63">1.3.5</A>, <A HREF="Reference-Manual009.html#@default411">7.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>Arguments Scope</TT>, <A HREF="Reference-Manual013.html#@default699">11.2.2</A>
</LI><LI CLASS="li-indexenv">Arithmetical notations, <A HREF="Reference-Manual005.html#@default259">3.2.2</A>
</LI><LI CLASS="li-indexenv">Arity, <A HREF="Reference-Manual006.html#@default324">4.5.3</A>
</LI><LI CLASS="li-indexenv">Associativity, <A HREF="Reference-Manual013.html#@default683">11.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>Axiom</TT>, <A HREF="Reference-Manual003.html#@default31">1.3.1</A>
</LI><LI CLASS="li-indexenv"><TT>Axiom </TT>(and coercions), <A HREF="Reference-Manual021.html#@default743">5</A>
</LI><LI CLASS="li-indexenv"><TT>abstract</TT>, <A HREF="Reference-Manual011.html#@default666">9.2</A>
</LI><LI CLASS="li-indexenv">abstractions, <A HREF="Reference-Manual003.html#@default21">1.2.7</A>
</LI><LI CLASS="li-indexenv"><TT>absurd</TT>, <A HREF="Reference-Manual005.html#@default154">3.1.2</A>, <A HREF="Reference-Manual010.html#@default483">8.4.1</A>
</LI><LI CLASS="li-indexenv"><TT>absurd_set</TT>, <A HREF="Reference-Manual005.html#@default221">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>all</TT>, <A HREF="Reference-Manual005.html#@default144">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>and</TT>, <A HREF="Reference-Manual005.html#@default134">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>and_rec</TT>, <A HREF="Reference-Manual005.html#@default222">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>app</TT>, <A HREF="Reference-Manual005.html#@default280">3.2.5</A>
</LI><LI CLASS="li-indexenv">applications, <A HREF="Reference-Manual003.html#@default23">1.2.9</A>
</LI><LI CLASS="li-indexenv"><TT>apply</TT>, <A HREF="Reference-Manual010.html#@default463">8.3.6</A>
</LI><LI CLASS="li-indexenv"><TT>apply &#X2026; with</TT>, <A HREF="Reference-Manual010.html#@default464">1</A>
</LI><LI CLASS="li-indexenv"><TT>apply </TT><TT>&#X2026;</TT><TT> in</TT>, <A HREF="Reference-Manual010.html#@default474">8.3.9</A>
</LI><LI CLASS="li-indexenv"><TT>assert</TT>, <A HREF="Reference-Manual010.html#@default469">8.3.8</A>
</LI><LI CLASS="li-indexenv"><TT>assert as</TT>, <A HREF="Reference-Manual010.html#@default473">5</A>
</LI><LI CLASS="li-indexenv"><TT>assert by</TT>, <A HREF="Reference-Manual010.html#@default472">4</A>
</LI><LI CLASS="li-indexenv"><TT>assumption</TT>, <A HREF="Reference-Manual010.html#@default447">8.3.1</A>
</LI><LI CLASS="li-indexenv"><TT>auto</TT>, <A HREF="Reference-Manual010.html#@default578">8.12.1</A>
</LI><LI CLASS="li-indexenv"><TT>autorewrite</TT>, <A HREF="Reference-Manual010.html#@default599">8.12.12</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>Back</TT>, <A HREF="Reference-Manual008.html#@default384">6.6.2</A>
</LI><LI CLASS="li-indexenv"><TT>Bad Magic Number</TT>, <A HREF="Reference-Manual008.html#@default367">3</A>
</LI><LI CLASS="li-indexenv"><TT>Begin Silent</TT>, <A HREF="Reference-Manual008.html#@default391">6.8.1</A>
</LI><LI CLASS="li-indexenv"><TT>Bind Scope</TT>, <A HREF="Reference-Manual013.html#@default700">11.2.2</A>
</LI><LI CLASS="li-indexenv">Binding list, <A HREF="Reference-Manual010.html#@default480">8.3.12</A>
</LI><LI CLASS="li-indexenv">BNF metasyntax, <A HREF="Reference-Manual003.html#@default1">1</A>
</LI><LI CLASS="li-indexenv">&#X3B2;-reduction, <A HREF="Reference-Manual006.html#@default310">4.3</A>, <A HREF="Reference-Manual006.html#@default314">4.3</A>
</LI><LI CLASS="li-indexenv">binders, <A HREF="Reference-Manual003.html#@default20">1.2.6</A>
</LI><LI CLASS="li-indexenv"><TT>bool</TT>, <A HREF="Reference-Manual005.html#@default168">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>bool_choice</TT>, <A HREF="Reference-Manual005.html#@default214">3.1.4</A>
</LI><LI CLASS="li-indexenv">byte-code, <A HREF="Reference-Manual015.html#@default707">12.1</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Calculus of
(Co)Inductive Constructions, <A HREF="Reference-Manual006.html#@default291">4</A>
</LI><LI CLASS="li-indexenv">Calculus of (Co)Inductive Constructions, <A HREF="Reference-Manual006.html#@default290">4</A>
</LI><LI CLASS="li-indexenv"><TT>Canonical Structure</TT>, <A HREF="Reference-Manual004.html#@default119">2.7.11</A>
</LI><LI CLASS="li-indexenv"><TT>Cases</TT>, <A HREF="Reference-Manual020.html#@default730">15</A>
</LI><LI CLASS="li-indexenv">Cast, <A HREF="Reference-Manual003.html#@default24">1.2.10</A>
</LI><LI CLASS="li-indexenv"><TT>Cd</TT>, <A HREF="Reference-Manual008.html#@default373">6.5.2</A>
</LI><LI CLASS="li-indexenv"><TT>Check</TT>, <A HREF="Reference-Manual008.html#@default344">6.2.1</A>
</LI><LI CLASS="li-indexenv"><TT>Choice</TT>, <A HREF="Reference-Manual005.html#@default212">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>Choice2</TT>, <A HREF="Reference-Manual005.html#@default213">3.1.4</A>
</LI><LI CLASS="li-indexenv"><SPAN STYLE="font-variant:small-caps">CIC</SPAN>, <A HREF="Reference-Manual006.html#@default288">4</A>
</LI><LI CLASS="li-indexenv">Clauses, <A HREF="Reference-Manual010.html#@default486">8.5</A>
</LI><LI CLASS="li-indexenv"><TT>Close Scope</TT>, <A HREF="Reference-Manual013.html#@default696">11.2.1</A>
</LI><LI CLASS="li-indexenv"><TT>Coercion</TT>, <A HREF="Reference-Manual004.html#@default122">2.8</A>, <A HREF="Reference-Manual021.html#@default738">16.6.1</A>, <A HREF="Reference-Manual021.html#@default740">2</A>
</LI><LI CLASS="li-indexenv"><TT>Coercion Local</TT>, <A HREF="Reference-Manual021.html#@default739">1</A>, <A HREF="Reference-Manual021.html#@default741">4</A>
</LI><LI CLASS="li-indexenv">Coercions, <A HREF="Reference-Manual004.html#@default121">2.8</A>
<UL CLASS="indexenv"><LI CLASS="li-indexenv">
and records, <A HREF="Reference-Manual021.html#@default758">16.9</A>
</LI><LI CLASS="li-indexenv">and sections, <A HREF="Reference-Manual021.html#@default760">16.10</A>
</LI><LI CLASS="li-indexenv">classes, <A HREF="Reference-Manual021.html#@default733">16.2</A>
</LI><LI CLASS="li-indexenv">Funclass, <A HREF="Reference-Manual021.html#@default734">16.3</A>
</LI><LI CLASS="li-indexenv">identity, <A HREF="Reference-Manual021.html#@default736">16.4</A>
</LI><LI CLASS="li-indexenv">inheritance graph, <A HREF="Reference-Manual021.html#@default737">16.5</A>
</LI><LI CLASS="li-indexenv">presentation, <A HREF="Reference-Manual021.html#@default732">16</A>
</LI><LI CLASS="li-indexenv">Sortclass, <A HREF="Reference-Manual021.html#@default735">16.3</A>
</LI></UL>
</LI><LI CLASS="li-indexenv"><TT>CoFixpoint</TT>, <A HREF="Reference-Manual003.html#@default51">1.3.4</A>
</LI><LI CLASS="li-indexenv"><TT>CoFixpoint </TT><TT>&#X2026;</TT><TT> where </TT><TT>&#X2026;</TT>, <A HREF="Reference-Manual013.html#@default689">11.1.8</A>
</LI><LI CLASS="li-indexenv"><TT>CoInductive</TT>, <A HREF="Reference-Manual003.html#@default49">1.3.3</A>
</LI><LI CLASS="li-indexenv"><TT>CoInductive </TT>(and coercions), <A HREF="Reference-Manual021.html#@default747">6</A>
</LI><LI CLASS="li-indexenv">Comments, <A HREF="Reference-Manual003.html#@default3">1.1</A>
</LI><LI CLASS="li-indexenv">Compiled files, <A HREF="Reference-Manual008.html#@default364">6.4</A>
</LI><LI CLASS="li-indexenv"><TT>Conjecture</TT>, <A HREF="Reference-Manual003.html#@default34">1.3.1</A>
</LI><LI CLASS="li-indexenv">Connectives, <A HREF="Reference-Manual005.html#@default129">3.1.2</A>
</LI><LI CLASS="li-indexenv">Constant, <A HREF="Reference-Manual003.html#@default41">1.3.2</A>
</LI><LI CLASS="li-indexenv">Context, <A HREF="Reference-Manual006.html#@default299">4.2</A>
</LI><LI CLASS="li-indexenv">Contributions, <A HREF="Reference-Manual005.html#@default287">3.3</A>
</LI><LI CLASS="li-indexenv">Conversion rules, <A HREF="Reference-Manual006.html#@default309">4.3</A>
</LI><LI CLASS="li-indexenv">Conversion tactics, <A HREF="Reference-Manual010.html#@default485">8.5</A>
</LI><LI CLASS="li-indexenv"><TT>coqdep</TT>, <A HREF="Reference-Manual016.html#@default715">13.2</A>
</LI><LI CLASS="li-indexenv"><FONT COLOR=purple>coqdoc</FONT>, <A HREF="Reference-Manual016.html#@default718">13.4</A>
</LI><LI CLASS="li-indexenv"><TT>coq_Makefile</TT>, <A HREF="Reference-Manual016.html#@default717">13.3</A>
</LI><LI CLASS="li-indexenv"><TT>coqmktop</TT>, <A HREF="Reference-Manual016.html#@default712">13.1</A>
</LI><LI CLASS="li-indexenv"><TT>coq-tex</TT>, <A HREF="Reference-Manual016.html#@default723">13.6</A>
</LI><LI CLASS="li-indexenv"><TT>Corollary</TT>, <A HREF="Reference-Manual003.html#@default57">1</A>
</LI><LI CLASS="li-indexenv"><TT>case</TT>, <A HREF="Reference-Manual010.html#@default513">5</A>
</LI><LI CLASS="li-indexenv"><TT>case &#X2026; with</TT>, <A HREF="Reference-Manual010.html#@default514">6</A>
</LI><LI CLASS="li-indexenv"><TT>cbv</TT>, <A HREF="Reference-Manual010.html#@default487">8.5.1</A>
</LI><LI CLASS="li-indexenv"><TT>change</TT>, <A HREF="Reference-Manual010.html#@default477">8.3.11</A>
</LI><LI CLASS="li-indexenv"><TT>change &#X2026; in</TT>, <A HREF="Reference-Manual010.html#@default479">8.3.11</A>
</LI><LI CLASS="li-indexenv"><TT>classical_left</TT>, <A HREF="Reference-Manual010.html#@default576">8.11.1</A>
</LI><LI CLASS="li-indexenv"><TT>classical_right</TT>, <A HREF="Reference-Manual010.html#@default577">8.11.1</A>
</LI><LI CLASS="li-indexenv"><TT>clear</TT>, <A HREF="Reference-Manual010.html#@default450">8.3.2</A>
</LI><LI CLASS="li-indexenv"><TT>clearbody</TT>, <A HREF="Reference-Manual010.html#@default451">2</A>
</LI><LI CLASS="li-indexenv"><TT>compare</TT>, <A HREF="Reference-Manual010.html#@default540">8.9.2</A>
</LI><LI CLASS="li-indexenv"><TT>compute</TT>, <A HREF="Reference-Manual010.html#@default489">8.5.1</A>, <A HREF="Reference-Manual010.html#@default491">1</A>
</LI><LI CLASS="li-indexenv"><TT>congruence</TT>, <A HREF="Reference-Manual010.html#@default589">8.12.7</A>
</LI><LI CLASS="li-indexenv"><TT>conj</TT>, <A HREF="Reference-Manual005.html#@default135">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>constructor</TT>, <A HREF="Reference-Manual010.html#@default501">8.6.1</A>
</LI><LI CLASS="li-indexenv"><TT>constructor &#X2026;  with</TT>, <A HREF="Reference-Manual010.html#@default502">2</A>
</LI><LI CLASS="li-indexenv">context<UL CLASS="indexenv"><LI CLASS="li-indexenv">
in expression, <A HREF="Reference-Manual011.html#@default657">9.2</A>
</LI><LI CLASS="li-indexenv">in pattern, <A HREF="Reference-Manual011.html#@default646">1</A>
</LI></UL>
</LI><LI CLASS="li-indexenv"><TT>contradiction</TT>, <A HREF="Reference-Manual010.html#@default484">8.4.2</A>
</LI><LI CLASS="li-indexenv"><TT>coqc</TT>, <A HREF="Reference-Manual015.html#@default706">12</A>
</LI><LI CLASS="li-indexenv"><TT>coqide</TT>, <A HREF="Reference-Manual017.html#@default729">14</A>
</LI><LI CLASS="li-indexenv"><TT>coqtop</TT>, <A HREF="Reference-Manual015.html#@default705">12</A>
</LI><LI CLASS="li-indexenv"><TT>cut</TT>, <A HREF="Reference-Manual010.html#@default470">3</A>
</LI><LI CLASS="li-indexenv"><TT>cutrewrite</TT>, <A HREF="Reference-Manual010.html#@default528">8.8.2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Datatypes, <A HREF="Reference-Manual005.html#@default164">3.1.3</A>
</LI><LI CLASS="li-indexenv">Debugger, <A HREF="Reference-Manual016.html#@default713">13.1</A>
</LI><LI CLASS="li-indexenv">Declarations, <A HREF="Reference-Manual003.html#@default30">1.3.1</A>
</LI><LI CLASS="li-indexenv"><TT>Declare Implicit Tactic</TT>, <A HREF="Reference-Manual010.html#@default611">8.13.6</A>
</LI><LI CLASS="li-indexenv"><TT>Declare Left Step</TT>, <A HREF="Reference-Manual010.html#@default536">8.8.8</A>
</LI><LI CLASS="li-indexenv"><TT>Declare ML Module</TT>, <A HREF="Reference-Manual008.html#@default369">6.4.3</A>
</LI><LI CLASS="li-indexenv"><TT>Declare Right Step</TT>, <A HREF="Reference-Manual010.html#@default538">8.8.8</A>
</LI><LI CLASS="li-indexenv"><TT>Defined</TT>, <A HREF="Reference-Manual003.html#@default60">1.3.5</A>, <A HREF="Reference-Manual009.html#@default409">1</A>
</LI><LI CLASS="li-indexenv"><TT>Definition</TT>, <A HREF="Reference-Manual003.html#@default43">1.3.2</A>, <A HREF="Reference-Manual009.html#@default416">3</A>
</LI><LI CLASS="li-indexenv">Definitions, <A HREF="Reference-Manual003.html#@default39">1.3.2</A>
</LI><LI CLASS="li-indexenv"><TT>Delimit Scope</TT>, <A HREF="Reference-Manual013.html#@default698">11.2.2</A>
</LI><LI CLASS="li-indexenv">Dependencies, <A HREF="Reference-Manual016.html#@default714">13.2</A>
</LI><LI CLASS="li-indexenv"><TT>Derive Dependent Inversion</TT>, <A HREF="Reference-Manual010.html#@default572">2</A>
</LI><LI CLASS="li-indexenv"><TT>Derive Dependent Inversion_clear</TT>, <A HREF="Reference-Manual010.html#@default573">3</A>
</LI><LI CLASS="li-indexenv"><TT>Derive Inversion</TT>, <A HREF="Reference-Manual010.html#@default569">8.10.2</A>
</LI><LI CLASS="li-indexenv"><TT>Derive Inversion_clear</TT>, <A HREF="Reference-Manual010.html#@default570">1</A>
</LI><LI CLASS="li-indexenv">Derive Inversion_clear &#X2026; with, <A HREF="Reference-Manual010.html#@default571">1</A>
</LI><LI CLASS="li-indexenv"><TT>Drop</TT>, <A HREF="Reference-Manual008.html#@default389">6.7.2</A>
</LI><LI CLASS="li-indexenv"><TT>decide equality</TT>, <A HREF="Reference-Manual010.html#@default539">8.9.1</A>
</LI><LI CLASS="li-indexenv"><TT>decompose</TT>, <A HREF="Reference-Manual010.html#@default518">8.7.5</A>
</LI><LI CLASS="li-indexenv"><TT>decompose record</TT>, <A HREF="Reference-Manual010.html#@default520">2</A>
</LI><LI CLASS="li-indexenv"><TT>decompose sum</TT>, <A HREF="Reference-Manual010.html#@default519">1</A>
</LI><LI CLASS="li-indexenv">&#X3B4;-reduction, <A HREF="Reference-Manual003.html#@default40">1.3.2</A>, <A HREF="Reference-Manual006.html#@default312">4.3</A>, <A HREF="Reference-Manual006.html#@default316">4.3</A>
</LI><LI CLASS="li-indexenv"><TT>dependent inversion</TT>, <A HREF="Reference-Manual010.html#@default557">10</A>
</LI><LI CLASS="li-indexenv"><TT>dependent inversion &#X2026; as </TT>, <A HREF="Reference-Manual010.html#@default558">11</A>
</LI><LI CLASS="li-indexenv"><TT>dependent inversion &#X2026; as &#X2026; with</TT>, <A HREF="Reference-Manual010.html#@default562">15</A>
</LI><LI CLASS="li-indexenv"><TT>dependent inversion &#X2026; with</TT>, <A HREF="Reference-Manual010.html#@default561">14</A>
</LI><LI CLASS="li-indexenv"><TT>dependent inversion_clear</TT>, <A HREF="Reference-Manual010.html#@default559">12</A>
</LI><LI CLASS="li-indexenv"><TT>dependent inversion_clear &#X2026; as</TT>, <A HREF="Reference-Manual010.html#@default560">13</A>
</LI><LI CLASS="li-indexenv"><TT>dependent inversion_clear &#X2026; as &#X2026; with</TT>, <A HREF="Reference-Manual010.html#@default564">17</A>
</LI><LI CLASS="li-indexenv"><TT>dependent inversion_clear &#X2026; with</TT>, <A HREF="Reference-Manual010.html#@default563">16</A>
</LI><LI CLASS="li-indexenv"><TT>dependent rewrite -&gt;</TT>, <A HREF="Reference-Manual010.html#@default547">8.9.6</A>
</LI><LI CLASS="li-indexenv"><TT>dependent rewrite &lt;-</TT>, <A HREF="Reference-Manual010.html#@default548">1</A>
</LI><LI CLASS="li-indexenv"><TT>destruct</TT>, <A HREF="Reference-Manual010.html#@default512">8.7.2</A>
</LI><LI CLASS="li-indexenv"><TT>discriminate</TT>, <A HREF="Reference-Manual010.html#@default541">8.9.3</A>, <A HREF="Reference-Manual010.html#@default542">2</A>
</LI><LI CLASS="li-indexenv"><TT>discrR</TT>, <A HREF="Reference-Manual005.html#@default273">3.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>do</TT>, <A HREF="Reference-Manual011.html#@default621">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>double induction</TT>, <A HREF="Reference-Manual010.html#@default517">8.7.4</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Elimination<UL CLASS="indexenv"><LI CLASS="li-indexenv">
Empty elimination, <A HREF="Reference-Manual006.html#@default330">4.5.4</A>
</LI><LI CLASS="li-indexenv">Singleton elimination, <A HREF="Reference-Manual006.html#@default329">4.5.4</A>
</LI></UL>
</LI><LI CLASS="li-indexenv">Elimination sorts, <A HREF="Reference-Manual006.html#@default328">4.5.4</A>
</LI><LI CLASS="li-indexenv">Emacs, <A HREF="Reference-Manual016.html#@default725">13.7</A>
</LI><LI CLASS="li-indexenv"><TT>End</TT>, <A HREF="Reference-Manual004.html#@default90">2.4.2</A>, <A HREF="Reference-Manual004.html#@default93">2.5.2</A>, <A HREF="Reference-Manual004.html#@default96">2.5.5</A>
</LI><LI CLASS="li-indexenv"><TT>End Silent</TT>, <A HREF="Reference-Manual008.html#@default393">6.8.2</A>
</LI><LI CLASS="li-indexenv">Environment, <A HREF="Reference-Manual003.html#@default42">1.3.2</A>, <A HREF="Reference-Manual006.html#@default300">4.2</A>
</LI><LI CLASS="li-indexenv">Environment variables, <A HREF="Reference-Manual015.html#@default710">12.4</A>
</LI><LI CLASS="li-indexenv">Equality, <A HREF="Reference-Manual005.html#@default151">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>Eval</TT>, <A HREF="Reference-Manual008.html#@default345">6.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>Example</TT>, <A HREF="Reference-Manual003.html#@default44">3</A>
</LI><LI CLASS="li-indexenv"><TT>Exc</TT>, <A HREF="Reference-Manual005.html#@default215">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>Except</TT>, <A HREF="Reference-Manual005.html#@default220">3.1.4</A>
</LI><LI CLASS="li-indexenv">Explicitation of implicit arguments, <A HREF="Reference-Manual004.html#@default114">2.7.7</A>
</LI><LI CLASS="li-indexenv"><TT>Export</TT>, <A HREF="Reference-Manual004.html#@default98">1</A>
</LI><LI CLASS="li-indexenv"><TT>Extract Constant</TT>, <A HREF="Reference-Manual023.html#@default776">18.2.3</A>
</LI><LI CLASS="li-indexenv"><TT>Extract Inductive</TT>, <A HREF="Reference-Manual023.html#@default777">18.2.3</A>
</LI><LI CLASS="li-indexenv">Extraction, <A HREF="Reference-Manual023.html#@default762">18</A>
</LI><LI CLASS="li-indexenv"><TT>Extraction</TT>, <A HREF="Reference-Manual008.html#@default346">6.2.3</A>, <A HREF="Reference-Manual023.html#@default763">18.1</A>
</LI><LI CLASS="li-indexenv"><TT>Extraction Inline</TT>, <A HREF="Reference-Manual023.html#@default772">18.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>Extraction Language</TT>, <A HREF="Reference-Manual023.html#@default767">18.2.1</A>
</LI><LI CLASS="li-indexenv"><TT>Extraction Module</TT>, <A HREF="Reference-Manual023.html#@default765">18.1</A>
</LI><LI CLASS="li-indexenv"><TT>Extraction NoInline</TT>, <A HREF="Reference-Manual023.html#@default773">18.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>eapply</TT>, <A HREF="Reference-Manual010.html#@default465">3</A>, <A HREF="Reference-Manual012.html#@default675">10.2</A>
</LI><LI CLASS="li-indexenv"><TT>eassumption</TT>, <A HREF="Reference-Manual010.html#@default449">8.3.1</A>
</LI><LI CLASS="li-indexenv"><TT>eauto</TT>, <A HREF="Reference-Manual010.html#@default580">8.12.2</A>
</LI><LI CLASS="li-indexenv"><TT>eexact</TT>, <A HREF="Reference-Manual010.html#@default443">1</A>
</LI><LI CLASS="li-indexenv"><TT>elim &#X2026; using</TT>, <A HREF="Reference-Manual010.html#@default509">9</A>
</LI><LI CLASS="li-indexenv"><TT>elim &#X2026; with</TT>, <A HREF="Reference-Manual010.html#@default508">7</A>
</LI><LI CLASS="li-indexenv"><TT>elimtype</TT>, <A HREF="Reference-Manual010.html#@default510">10</A>
</LI><LI CLASS="li-indexenv"><TT>eq</TT>, <A HREF="Reference-Manual005.html#@default152">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>eq_add_S</TT>, <A HREF="Reference-Manual005.html#@default226">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>eq_ind_r</TT>, <A HREF="Reference-Manual005.html#@default159">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>eq_rec</TT>, <A HREF="Reference-Manual005.html#@default219">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>eq_rec_r</TT>, <A HREF="Reference-Manual005.html#@default160">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>eq_rect</TT>, <A HREF="Reference-Manual005.html#@default161">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>eq_rect_r</TT>, <A HREF="Reference-Manual005.html#@default162">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>eq_S</TT>, <A HREF="Reference-Manual005.html#@default223">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>error</TT>, <A HREF="Reference-Manual005.html#@default217">3.1.4</A>
</LI><LI CLASS="li-indexenv">&#X3B7;-conversion, <A HREF="Reference-Manual006.html#@default319">4.3</A>
</LI><LI CLASS="li-indexenv">&#X3B7;-reduction, <A HREF="Reference-Manual006.html#@default320">4.3</A>
</LI><LI CLASS="li-indexenv">eval<UL CLASS="indexenv"><LI CLASS="li-indexenv">
in Ltac, <A HREF="Reference-Manual011.html#@default661">9.2</A>
</LI></UL>
</LI><LI CLASS="li-indexenv"><TT>evar</TT>, <A HREF="Reference-Manual010.html#@default481">8.3.13</A>
</LI><LI CLASS="li-indexenv"><TT>ex</TT>, <A HREF="Reference-Manual005.html#@default145">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>ex2</TT>, <A HREF="Reference-Manual005.html#@default148">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>ex_intro</TT>, <A HREF="Reference-Manual005.html#@default147">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>ex_intro2</TT>, <A HREF="Reference-Manual005.html#@default150">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>exact</TT>, <A HREF="Reference-Manual010.html#@default442">8.2.1</A>
</LI><LI CLASS="li-indexenv"><TT>exist</TT>, <A HREF="Reference-Manual005.html#@default193">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>exist2</TT>, <A HREF="Reference-Manual005.html#@default195">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>existS</TT>, <A HREF="Reference-Manual005.html#@default199">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>existS2</TT>, <A HREF="Reference-Manual005.html#@default203">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>exists</TT>, <A HREF="Reference-Manual005.html#@default146">3.1.2</A>, <A HREF="Reference-Manual010.html#@default504">4</A>
</LI><LI CLASS="li-indexenv"><TT>exists2</TT>, <A HREF="Reference-Manual005.html#@default149">3.1.2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>Fact</TT>, <A HREF="Reference-Manual003.html#@default55">1.3.5</A>, <A HREF="Reference-Manual009.html#@default415">2</A>
</LI><LI CLASS="li-indexenv"><TT>False</TT>, <A HREF="Reference-Manual005.html#@default132">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>False_rec</TT>, <A HREF="Reference-Manual005.html#@default218">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>Fix</TT>, <A HREF="Reference-Manual006.html#@default333">4.5.5</A>
</LI><LI CLASS="li-indexenv"><TT>Fix_F</TT>, <A HREF="Reference-Manual005.html#@default252">3.1.6</A>
</LI><LI CLASS="li-indexenv"><TT>Fix_F_eq</TT>, <A HREF="Reference-Manual005.html#@default255">3.1.6</A>
</LI><LI CLASS="li-indexenv"><TT>Fix_F_inv</TT>, <A HREF="Reference-Manual005.html#@default254">3.1.6</A>
</LI><LI CLASS="li-indexenv"><TT>Fixpoint</TT>, <A HREF="Reference-Manual003.html#@default50">1.3.4</A>
</LI><LI CLASS="li-indexenv"><TT>Fixpoint </TT><TT>&#X2026;</TT><TT> where </TT><TT>&#X2026;</TT>, <A HREF="Reference-Manual013.html#@default688">11.1.8</A>
</LI><LI CLASS="li-indexenv"><TT>Focus</TT>, <A HREF="Reference-Manual009.html#@default426">7.2.5</A>
</LI><LI CLASS="li-indexenv"><TT>Function</TT>, <A HREF="Reference-Manual004.html#@default87">2.3</A>
</LI><LI CLASS="li-indexenv"><TT>Functional Scheme</TT>, <A HREF="Reference-Manual010.html#@default613">8.15</A>, <A HREF="Reference-Manual012.html#@default677">10.4</A>
</LI><LI CLASS="li-indexenv"><TT>f_equal</TT>, <A HREF="Reference-Manual005.html#@default157">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>f_equal</TT><TT><I>i</I></TT>, <A HREF="Reference-Manual005.html#@default163">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>fail</TT>, <A HREF="Reference-Manual011.html#@default636">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>false</TT>, <A HREF="Reference-Manual005.html#@default170">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>field</TT>, <A HREF="Reference-Manual010.html#@default594">8.12.10</A>, <A HREF="Reference-Manual025.html#@default786">20.7</A>
</LI><LI CLASS="li-indexenv"><TT>field_simplify</TT>, <A HREF="Reference-Manual010.html#@default595">8.12.10</A>, <A HREF="Reference-Manual025.html#@default787">20.7</A>
</LI><LI CLASS="li-indexenv"><TT>field_simplify_eq</TT>, <A HREF="Reference-Manual010.html#@default596">8.12.10</A>, <A HREF="Reference-Manual025.html#@default788">20.7</A>
</LI><LI CLASS="li-indexenv"><TT>first</TT>, <A HREF="Reference-Manual011.html#@default630">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>firstorder</TT>, <A HREF="Reference-Manual010.html#@default584">8.12.6</A>
</LI><LI CLASS="li-indexenv"><TT>firstorder </TT><I><FONT COLOR=maroon>tactic</FONT></I>, <A HREF="Reference-Manual010.html#@default585">1</A>
</LI><LI CLASS="li-indexenv"><TT>firstorder using</TT>, <A HREF="Reference-Manual010.html#@default587">3</A>
</LI><LI CLASS="li-indexenv"><TT>firstorder with</TT>, <A HREF="Reference-Manual010.html#@default586">2</A>
</LI><LI CLASS="li-indexenv">fix <I><FONT COLOR=maroon>ident</FONT></I><SUB><I>i</I></SUB>{&#X2026;}, <A HREF="Reference-Manual003.html#@default29">1.2.14</A>
</LI><LI CLASS="li-indexenv"><TT>fix_eq</TT>, <A HREF="Reference-Manual005.html#@default253">3.1.6</A>
</LI><LI CLASS="li-indexenv"><TT>flat_map</TT>, <A HREF="Reference-Manual005.html#@default284">3.2.5</A>
</LI><LI CLASS="li-indexenv"><TT>fold</TT>, <A HREF="Reference-Manual010.html#@default499">8.5.6</A>
</LI><LI CLASS="li-indexenv"><TT>fold_left</TT>, <A HREF="Reference-Manual005.html#@default285">3.2.5</A>
</LI><LI CLASS="li-indexenv"><TT>fold_right</TT>, <A HREF="Reference-Manual005.html#@default286">3.2.5</A>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>form</FONT></I>, <A HREF="Reference-Manual003.html#@default17">1.2.5</A>
</LI><LI CLASS="li-indexenv"><TT>fourier</TT>, <A HREF="Reference-Manual010.html#@default598">8.12.11</A>
</LI><LI CLASS="li-indexenv">fresh<UL CLASS="indexenv"><LI CLASS="li-indexenv">
in Ltac, <A HREF="Reference-Manual011.html#@default659">9.2</A>
</LI></UL>
</LI><LI CLASS="li-indexenv"><TT>fst</TT>, <A HREF="Reference-Manual005.html#@default188">3.1.3</A>
</LI><LI CLASS="li-indexenv">fun<UL CLASS="indexenv"><LI CLASS="li-indexenv">
in Ltac, <A HREF="Reference-Manual011.html#@default642">9.2</A>
</LI></UL>
</LI><LI CLASS="li-indexenv"><TT>functional induction</TT>, <A HREF="Reference-Manual010.html#@default521">8.7.6</A>, <A HREF="Reference-Manual012.html#@default678">10.4</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Gallina, <A HREF="Reference-Manual003.html#@default0">1</A>, <A HREF="Reference-Manual004.html#@default64">2</A>
</LI><LI CLASS="li-indexenv"><TT>gallina</TT>, <A HREF="Reference-Manual016.html#@default727">13.8</A>
</LI><LI CLASS="li-indexenv"><TT>Goal</TT>, <A HREF="Reference-Manual003.html#@default62">1.3.5</A>, <A HREF="Reference-Manual009.html#@default407">7.1.1</A>
</LI><LI CLASS="li-indexenv"><TT>ge</TT>, <A HREF="Reference-Manual005.html#@default241">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>generalize</TT>, <A HREF="Reference-Manual010.html#@default475">8.3.10</A>
</LI><LI CLASS="li-indexenv"><TT>generalize dependent</TT>, <A HREF="Reference-Manual010.html#@default476">2</A>
</LI><LI CLASS="li-indexenv">goal, <A HREF="Reference-Manual010.html#@default439">8</A>
</LI><LI CLASS="li-indexenv"><TT>gt</TT>, <A HREF="Reference-Manual005.html#@default242">3.1.5</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Head normal form, <A HREF="Reference-Manual006.html#@default322">4.3</A>
</LI><LI CLASS="li-indexenv"><TT>Hint</TT>, <A HREF="Reference-Manual010.html#@default601">8.13.1</A>
</LI><LI CLASS="li-indexenv"><TT>Hint Constructors</TT>, <A HREF="Reference-Manual010.html#@default604">8.13.1</A>
</LI><LI CLASS="li-indexenv"><TT>Hint Extern</TT>, <A HREF="Reference-Manual010.html#@default606">8.13.1</A>
</LI><LI CLASS="li-indexenv"><TT>Hint Immediate</TT>, <A HREF="Reference-Manual010.html#@default603">8.13.1</A>
</LI><LI CLASS="li-indexenv"><TT>Hint Resolve</TT>, <A HREF="Reference-Manual010.html#@default602">8.13.1</A>
</LI><LI CLASS="li-indexenv"><TT>Hint Rewrite</TT>, <A HREF="Reference-Manual010.html#@default609">8.13.4</A>
</LI><LI CLASS="li-indexenv"><TT>Hint Unfold</TT>, <A HREF="Reference-Manual010.html#@default605">8.13.1</A>
</LI><LI CLASS="li-indexenv">Hints databases, <A HREF="Reference-Manual010.html#@default600">8.13.1</A>
</LI><LI CLASS="li-indexenv"><TT>Hypotheses</TT>, <A HREF="Reference-Manual003.html#@default38">1.3.1</A>
</LI><LI CLASS="li-indexenv"><TT>Hypothesis</TT>, <A HREF="Reference-Manual003.html#@default37">1.3.1</A>
</LI><LI CLASS="li-indexenv"><TT>Hypothesis </TT>(and coercions), <A HREF="Reference-Manual021.html#@default745">5</A>
</LI><LI CLASS="li-indexenv"><TT>head</TT>, <A HREF="Reference-Manual005.html#@default278">3.2.5</A>
</LI><LI CLASS="li-indexenv"><TT>hnf</TT>, <A HREF="Reference-Manual010.html#@default494">8.5.3</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>I</TT>, <A HREF="Reference-Manual005.html#@default131">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>Identity Coercion</TT>, <A HREF="Reference-Manual021.html#@default748">16.6.2</A>
</LI><LI CLASS="li-indexenv"><TT>IF_then_else</TT>, <A HREF="Reference-Manual005.html#@default142">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>Implicit Arguments</TT>, <A HREF="Reference-Manual004.html#@default107">2.7.2</A>
</LI><LI CLASS="li-indexenv">Implicit arguments, <A HREF="Reference-Manual004.html#@default106">2.7</A>
</LI><LI CLASS="li-indexenv"><TT>Import</TT>, <A HREF="Reference-Manual004.html#@default97">2.5.8</A>
</LI><LI CLASS="li-indexenv"><TT>Inductive</TT>, <A HREF="Reference-Manual003.html#@default47">1.3.3</A>
</LI><LI CLASS="li-indexenv"><TT>Inductive </TT>(and coercions), <A HREF="Reference-Manual021.html#@default746">6</A>
</LI><LI CLASS="li-indexenv"><TT>Inductive </TT><TT>&#X2026;</TT><TT> where </TT><TT>&#X2026;</TT>, <A HREF="Reference-Manual013.html#@default690">11.1.8</A>
</LI><LI CLASS="li-indexenv">Inductive definitions, <A HREF="Reference-Manual003.html#@default46">1.3.3</A>
</LI><LI CLASS="li-indexenv"><TT>Infix</TT>, <A HREF="Reference-Manual013.html#@default686">11.1.6</A>
</LI><LI CLASS="li-indexenv"><TT>Inspect</TT>, <A HREF="Reference-Manual008.html#@default342">1</A>
</LI><LI CLASS="li-indexenv">Interpretation scopes, <A HREF="Reference-Manual013.html#@default694">11.2</A>
</LI><LI CLASS="li-indexenv"><TT>IsSucc</TT>, <A HREF="Reference-Manual005.html#@default228">3.1.5</A>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>ident</FONT></I>, <A HREF="Reference-Manual003.html#@default4">1.1</A>
</LI><LI CLASS="li-indexenv"><TT>identity</TT>, <A HREF="Reference-Manual005.html#@default177">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>idtac</TT>, <A HREF="Reference-Manual011.html#@default634">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>if ... then ... else</TT>, <A HREF="Reference-Manual004.html#@default68">2.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>iff</TT>, <A HREF="Reference-Manual005.html#@default141">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>induction</TT>, <A HREF="Reference-Manual010.html#@default507">8.7.1</A>
</LI><LI CLASS="li-indexenv"><TT>info</TT>, <A HREF="Reference-Manual011.html#@default664">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>injection</TT>, <A HREF="Reference-Manual010.html#@default543">8.9.4</A>, <A HREF="Reference-Manual010.html#@default544">2</A>
</LI><LI CLASS="li-indexenv"><TT>injection &#X2026; as</TT>, <A HREF="Reference-Manual010.html#@default545">3</A>
</LI><LI CLASS="li-indexenv"><TT>inl</TT>, <A HREF="Reference-Manual005.html#@default182">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>inleft</TT>, <A HREF="Reference-Manual005.html#@default209">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>inr</TT>, <A HREF="Reference-Manual005.html#@default183">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>inright</TT>, <A HREF="Reference-Manual005.html#@default210">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>instantiate</TT>, <A HREF="Reference-Manual010.html#@default482">8.3.14</A>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>integer</FONT></I>, <A HREF="Reference-Manual003.html#@default6">1.1</A>
</LI><LI CLASS="li-indexenv"><TT>intro</TT>, <A HREF="Reference-Manual010.html#@default454">8.3.5</A>
</LI><LI CLASS="li-indexenv"><TT>intro ... after</TT>, <A HREF="Reference-Manual010.html#@default462">7</A>
</LI><LI CLASS="li-indexenv"><TT>intro after</TT>, <A HREF="Reference-Manual010.html#@default461">6</A>
</LI><LI CLASS="li-indexenv"><TT>intros</TT>, <A HREF="Reference-Manual010.html#@default458">1</A>
</LI><LI CLASS="li-indexenv"><TT>intros </TT><I><FONT COLOR=maroon>intro_pattern</FONT></I>, <A HREF="Reference-Manual010.html#@default516">8.7.3</A>
</LI><LI CLASS="li-indexenv"><TT>intros until</TT>, <A HREF="Reference-Manual010.html#@default459">4</A>, <A HREF="Reference-Manual010.html#@default460">5</A>
</LI><LI CLASS="li-indexenv"><TT>intuition</TT>, <A HREF="Reference-Manual010.html#@default582">8.12.4</A>
</LI><LI CLASS="li-indexenv"><TT>inversion</TT>, <A HREF="Reference-Manual010.html#@default549">8.10.1</A>, <A HREF="Reference-Manual012.html#@default679">10.5</A>
</LI><LI CLASS="li-indexenv"><TT>inversion &#X2026; as</TT>, <A HREF="Reference-Manual010.html#@default551">3</A>
</LI><LI CLASS="li-indexenv"><TT>inversion &#X2026; as &#X2026; in</TT>, <A HREF="Reference-Manual010.html#@default554">7</A>
</LI><LI CLASS="li-indexenv"><TT>inversion &#X2026; in</TT>, <A HREF="Reference-Manual010.html#@default553">6</A>
</LI><LI CLASS="li-indexenv"><TT>inversion &#X2026; using</TT>, <A HREF="Reference-Manual010.html#@default567">20</A>
</LI><LI CLASS="li-indexenv"><TT>inversion &#X2026; using &#X2026; in</TT>, <A HREF="Reference-Manual010.html#@default568">21</A>
</LI><LI CLASS="li-indexenv"><TT>inversion_clear</TT>, <A HREF="Reference-Manual010.html#@default550">2</A>
</LI><LI CLASS="li-indexenv"><TT>inversion_clear &#X2026; as &#X2026; in</TT>, <A HREF="Reference-Manual010.html#@default556">9</A>
</LI><LI CLASS="li-indexenv"><TT>inversion_clear &#X2026; in</TT>, <A HREF="Reference-Manual010.html#@default555">8</A>
</LI><LI CLASS="li-indexenv"><TT>inversion_cleardots as</TT>, <A HREF="Reference-Manual010.html#@default552">5</A>
</LI><LI CLASS="li-indexenv">&#X3B9;-reduction, <A HREF="Reference-Manual006.html#@default311">4.3</A>, <A HREF="Reference-Manual006.html#@default315">4.3</A>, <A HREF="Reference-Manual006.html#@default332">4.5.4</A>, <A HREF="Reference-Manual006.html#@default336">4.5.5</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">L<sup>A</sup>T<sub>E</sub>X, <A HREF="Reference-Manual016.html#@default724">13.6</A>
</LI><LI CLASS="li-indexenv"><TT>Lemma</TT>, <A HREF="Reference-Manual003.html#@default53">1.3.5</A>, <A HREF="Reference-Manual009.html#@default413">1</A>
</LI><LI CLASS="li-indexenv"><TT>Let</TT>, <A HREF="Reference-Manual003.html#@default45">1.3.2</A>, <A HREF="Reference-Manual009.html#@default417">4</A>
</LI><LI CLASS="li-indexenv">Lexical conventions, <A HREF="Reference-Manual003.html#@default2">1.1</A>
</LI><LI CLASS="li-indexenv">Libraries, <A HREF="Reference-Manual004.html#@default102">2.6.1</A>
</LI><LI CLASS="li-indexenv"><TT>Load</TT>, <A HREF="Reference-Manual008.html#@default362">6.3.1</A>
</LI><LI CLASS="li-indexenv"><TT>Load Verbose</TT>, <A HREF="Reference-Manual008.html#@default363">2</A>
</LI><LI CLASS="li-indexenv">Loadpath, <A HREF="Reference-Manual008.html#@default371">6.5</A>
</LI><LI CLASS="li-indexenv">Local definitions, <A HREF="Reference-Manual003.html#@default26">1.2.12</A>
</LI><LI CLASS="li-indexenv"><TT>Locate</TT>, <A HREF="Reference-Manual008.html#@default355">6.2.10</A>, <A HREF="Reference-Manual013.html#@default693">11.1.10</A>
</LI><LI CLASS="li-indexenv"><TT>Locate
File</TT>, <A HREF="Reference-Manual008.html#@default381">6.5.10</A>
</LI><LI CLASS="li-indexenv"><TT>Locate Library</TT>, <A HREF="Reference-Manual008.html#@default382">6.5.11</A>
</LI><LI CLASS="li-indexenv"><TT>Locate Module</TT>, <A HREF="Reference-Manual004.html#@default101">2.5.11</A>
</LI><LI CLASS="li-indexenv">Logical paths, <A HREF="Reference-Manual004.html#@default103">2.6.1</A>
</LI><LI CLASS="li-indexenv">Ltac<UL CLASS="indexenv"><LI CLASS="li-indexenv">
eval, <A HREF="Reference-Manual011.html#@default660">9.2</A>
</LI><LI CLASS="li-indexenv">external, <A HREF="Reference-Manual011.html#@default668">9.2</A>
</LI><LI CLASS="li-indexenv">fresh, <A HREF="Reference-Manual011.html#@default658">9.2</A>
</LI><LI CLASS="li-indexenv">fun, <A HREF="Reference-Manual011.html#@default643">9.2</A>
</LI><LI CLASS="li-indexenv">lazymatch, <A HREF="Reference-Manual011.html#@default648">2</A>
</LI><LI CLASS="li-indexenv">lazymatch goal, <A HREF="Reference-Manual011.html#@default654">9.2</A>
</LI><LI CLASS="li-indexenv">lazymatch reverse goal, <A HREF="Reference-Manual011.html#@default656">9.2</A>
</LI><LI CLASS="li-indexenv">let, <A HREF="Reference-Manual011.html#@default638">9.2</A>
</LI><LI CLASS="li-indexenv">let rec, <A HREF="Reference-Manual011.html#@default639">9.2</A>
</LI><LI CLASS="li-indexenv">match, <A HREF="Reference-Manual011.html#@default644">9.2</A>
</LI><LI CLASS="li-indexenv">match goal, <A HREF="Reference-Manual011.html#@default649">9.2</A>
</LI><LI CLASS="li-indexenv">match reverse goal, <A HREF="Reference-Manual011.html#@default650">9.2</A>
</LI><LI CLASS="li-indexenv">type of, <A HREF="Reference-Manual011.html#@default662">9.2</A>
</LI></UL>
</LI></UL></TD><TD VALIGN=top ALIGN=left><UL CLASS="indexenv"><LI CLASS="li-indexenv"><TT>Ltac</TT>, <A HREF="Reference-Manual011.html#@default669">9.3</A>
</LI><LI CLASS="li-indexenv">&#X3BB;-calculus, <A HREF="Reference-Manual006.html#@default297">5</A>
</LI><LI CLASS="li-indexenv"><TT>lapply</TT>, <A HREF="Reference-Manual010.html#@default466">4</A>
</LI><LI CLASS="li-indexenv"><TT>lazy</TT>, <A HREF="Reference-Manual010.html#@default488">8.5.1</A>
</LI><LI CLASS="li-indexenv">lazymatch<UL CLASS="indexenv"><LI CLASS="li-indexenv">
in Ltac, <A HREF="Reference-Manual011.html#@default647">2</A>
</LI></UL>
</LI><LI CLASS="li-indexenv">lazymatch goal<UL CLASS="indexenv"><LI CLASS="li-indexenv">
in Ltac, <A HREF="Reference-Manual011.html#@default653">9.2</A>
</LI></UL>
</LI><LI CLASS="li-indexenv">lazymatch reverse goal<UL CLASS="indexenv"><LI CLASS="li-indexenv">
in Ltac, <A HREF="Reference-Manual011.html#@default655">9.2</A>
</LI></UL>
</LI><LI CLASS="li-indexenv"><TT>le</TT>, <A HREF="Reference-Manual005.html#@default237">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>le_n</TT>, <A HREF="Reference-Manual005.html#@default238">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>le_S</TT>, <A HREF="Reference-Manual005.html#@default239">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>left</TT>, <A HREF="Reference-Manual005.html#@default205">3.1.4</A>, <A HREF="Reference-Manual010.html#@default505">5</A>
</LI><LI CLASS="li-indexenv"><TT>legacy field</TT>, <A HREF="Reference-Manual025.html#@default797">20.9.3</A>
</LI><LI CLASS="li-indexenv"><TT>legacy ring</TT>, <A HREF="Reference-Manual025.html#@default790">20.9.1</A>
</LI><LI CLASS="li-indexenv"><TT>length</TT>, <A HREF="Reference-Manual005.html#@default277">3.2.5</A>
</LI><LI CLASS="li-indexenv">let<UL CLASS="indexenv"><LI CLASS="li-indexenv">
in Ltac, <A HREF="Reference-Manual011.html#@default640">9.2</A>
</LI></UL>
</LI><LI CLASS="li-indexenv"><TT>let ... in</TT>, <A HREF="Reference-Manual004.html#@default69">2.2.3</A>
</LI><LI CLASS="li-indexenv">let rec<UL CLASS="indexenv"><LI CLASS="li-indexenv">
in Ltac, <A HREF="Reference-Manual011.html#@default641">9.2</A>
</LI></UL>
</LI><LI CLASS="li-indexenv">let-in, <A HREF="Reference-Manual003.html#@default27">1.2.12</A>
</LI><LI CLASS="li-indexenv">local context, <A HREF="Reference-Manual009.html#@default405">7</A>
</LI><LI CLASS="li-indexenv"><TT>lt</TT>, <A HREF="Reference-Manual005.html#@default240">3.1.5</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>Makefile</TT>, <A HREF="Reference-Manual016.html#@default716">13.3</A>
</LI><LI CLASS="li-indexenv">Man pages, <A HREF="Reference-Manual016.html#@default728">13.9</A>
</LI><LI CLASS="li-indexenv">ML-like patterns, <A HREF="Reference-Manual004.html#@default67">2.2.1</A>, <A HREF="Reference-Manual020.html#@default731">15</A>
</LI><LI CLASS="li-indexenv"><TT>Module</TT>, <A HREF="Reference-Manual004.html#@default92">2.5.1</A>, <A HREF="Reference-Manual004.html#@default94">2.5.3</A>
</LI><LI CLASS="li-indexenv"><TT>Module Type</TT>, <A HREF="Reference-Manual004.html#@default95">2.5.4</A>
</LI><LI CLASS="li-indexenv">Modules, <A HREF="Reference-Manual004.html#@default91">2.5</A>
</LI><LI CLASS="li-indexenv"><TT>Mutual Inductive</TT>, <A HREF="Reference-Manual003.html#@default48">1.3.3</A>
</LI><LI CLASS="li-indexenv"><TT>map</TT>, <A HREF="Reference-Manual005.html#@default283">3.2.5</A>
</LI><LI CLASS="li-indexenv">match<UL CLASS="indexenv"><LI CLASS="li-indexenv">
in Ltac, <A HREF="Reference-Manual011.html#@default645">9.2</A>
</LI></UL>
</LI><LI CLASS="li-indexenv"><TT>match&#X2026;with&#X2026;end</TT>, <A HREF="Reference-Manual003.html#@default28">1.2.13</A>, <A HREF="Reference-Manual004.html#@default66">2.2</A>, <A HREF="Reference-Manual006.html#@default327">4.5.4</A>
</LI><LI CLASS="li-indexenv">match goal<UL CLASS="indexenv"><LI CLASS="li-indexenv">
in Ltac, <A HREF="Reference-Manual011.html#@default651">9.2</A>
</LI></UL>
</LI><LI CLASS="li-indexenv">match reverse goal<UL CLASS="indexenv"><LI CLASS="li-indexenv">
in Ltac, <A HREF="Reference-Manual011.html#@default652">9.2</A>
</LI></UL>
</LI><LI CLASS="li-indexenv"><TT>mod</TT>, <A HREF="Reference-Manual005.html#@default269">3.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>move</TT>, <A HREF="Reference-Manual010.html#@default452">8.3.3</A>
</LI><LI CLASS="li-indexenv"><TT>mult</TT>, <A HREF="Reference-Manual005.html#@default234">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>mult_n_O</TT>, <A HREF="Reference-Manual005.html#@default235">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>mult_n_Sm</TT>, <A HREF="Reference-Manual005.html#@default236">3.1.5</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>None</TT>, <A HREF="Reference-Manual005.html#@default176">3.1.3</A>
</LI><LI CLASS="li-indexenv">Normal form, <A HREF="Reference-Manual006.html#@default321">4.3</A>
</LI><LI CLASS="li-indexenv"><TT>Notation</TT>, <A HREF="Reference-Manual013.html#@default681">11.1</A>, <A HREF="Reference-Manual013.html#@default703">11.3</A>
</LI><LI CLASS="li-indexenv">Notations for lists, <A HREF="Reference-Manual005.html#@default276">3.2.5</A>
</LI><LI CLASS="li-indexenv">Notations for real numbers, <A HREF="Reference-Manual005.html#@default272">3.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>n_Sn</TT>, <A HREF="Reference-Manual005.html#@default230">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>nat</TT>, <A HREF="Reference-Manual005.html#@default171">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>nat_case</TT>, <A HREF="Reference-Manual005.html#@default243">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>nat_double_ind</TT>, <A HREF="Reference-Manual005.html#@default244">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>nat_scope</TT>, <A HREF="Reference-Manual005.html#@default271">3.2.3</A>
</LI><LI CLASS="li-indexenv">native code, <A HREF="Reference-Manual015.html#@default708">12.1</A>
</LI><LI CLASS="li-indexenv"><TT>not</TT>, <A HREF="Reference-Manual005.html#@default133">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>not_eq_S</TT>, <A HREF="Reference-Manual005.html#@default227">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>notT</TT>, <A HREF="Reference-Manual005.html#@default256">3.1.7</A>
</LI><LI CLASS="li-indexenv"><TT>nth</TT>, <A HREF="Reference-Manual005.html#@default282">3.2.5</A>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>num</FONT></I>, <A HREF="Reference-Manual003.html#@default5">1.1</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>O</TT>, <A HREF="Reference-Manual005.html#@default172">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>O_S</TT>, <A HREF="Reference-Manual005.html#@default229">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>Opaque</TT>, <A HREF="Reference-Manual008.html#@default347">6.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Open Scope</TT>, <A HREF="Reference-Manual013.html#@default695">11.2.1</A>
</LI><LI CLASS="li-indexenv">Options of the command line, <A HREF="Reference-Manual015.html#@default711">12.5</A>
</LI><LI CLASS="li-indexenv"><TT>omega</TT>, <A HREF="Reference-Manual010.html#@default590">8.12.8</A>, <A HREF="Reference-Manual022.html#@default761">17.1</A>
</LI><LI CLASS="li-indexenv"><TT>option</TT>, <A HREF="Reference-Manual005.html#@default174">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>or</TT>, <A HREF="Reference-Manual005.html#@default138">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>or_introl</TT>, <A HREF="Reference-Manual005.html#@default139">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>or_intror</TT>, <A HREF="Reference-Manual005.html#@default140">3.1.2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>Parameter</TT>, <A HREF="Reference-Manual003.html#@default32">1.3.1</A>
</LI><LI CLASS="li-indexenv"><TT>Parameter </TT>(and coercions), <A HREF="Reference-Manual021.html#@default744">5</A>
</LI><LI CLASS="li-indexenv"><TT>Parameters</TT>, <A HREF="Reference-Manual003.html#@default33">1.3.1</A>
</LI><LI CLASS="li-indexenv">Peano's arithmetic, <A HREF="Reference-Manual005.html#@default270">3.2.3</A>
</LI><LI CLASS="li-indexenv">Positivity, <A HREF="Reference-Manual006.html#@default323">4.5.3</A>
</LI><LI CLASS="li-indexenv">Precedences, <A HREF="Reference-Manual013.html#@default682">11.1.2</A>
</LI><LI CLASS="li-indexenv">Predicative Calculus of
(Co)Inductive Constructions, <A HREF="Reference-Manual006.html#@default292">4</A>
</LI><LI CLASS="li-indexenv"><TT>Print</TT>, <A HREF="Reference-Manual008.html#@default338">6.1.1</A>
</LI><LI CLASS="li-indexenv"><TT>Print All</TT>, <A HREF="Reference-Manual008.html#@default341">6.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>Print Canonical Projections</TT>, <A HREF="Reference-Manual004.html#@default120">2.7.11</A>
</LI><LI CLASS="li-indexenv"><TT>Print Classes</TT>, <A HREF="Reference-Manual021.html#@default750">16.7.1</A>
</LI><LI CLASS="li-indexenv"><TT>Print Coercion Paths</TT>, <A HREF="Reference-Manual021.html#@default753">16.7.4</A>
</LI><LI CLASS="li-indexenv"><TT>Print Coercions</TT>, <A HREF="Reference-Manual021.html#@default751">16.7.2</A>
</LI><LI CLASS="li-indexenv"><TT>Print Extraction Inline</TT>, <A HREF="Reference-Manual023.html#@default774">18.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>Print Grammar constr</TT>, <A HREF="Reference-Manual013.html#@default684">11.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>Print Grammar pattern</TT>, <A HREF="Reference-Manual013.html#@default685">11.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>Print Graph</TT>, <A HREF="Reference-Manual021.html#@default752">16.7.3</A>
</LI><LI CLASS="li-indexenv"><TT>Print Hint</TT>, <A HREF="Reference-Manual010.html#@default607">8.13.3</A>
</LI><LI CLASS="li-indexenv"><TT>Print HintDb</TT>, <A HREF="Reference-Manual010.html#@default608">3</A>
</LI><LI CLASS="li-indexenv"><TT>Print Implicit</TT>, <A HREF="Reference-Manual004.html#@default116">2.7.8</A>
</LI><LI CLASS="li-indexenv"><TT>Print LoadPath</TT>, <A HREF="Reference-Manual008.html#@default377">6.5.6</A>
</LI><LI CLASS="li-indexenv"><TT>Print Ltac</TT>, <A HREF="Reference-Manual011.html#@default670">9.3.2</A>
</LI><LI CLASS="li-indexenv"><TT>Print ML Modules</TT>, <A HREF="Reference-Manual008.html#@default370">6.4.4</A>
</LI><LI CLASS="li-indexenv"><TT>Print ML Path</TT>, <A HREF="Reference-Manual008.html#@default380">6.5.9</A>
</LI><LI CLASS="li-indexenv"><TT>Print Module</TT>, <A HREF="Reference-Manual004.html#@default99">2.5.9</A>
</LI><LI CLASS="li-indexenv"><TT>Print Module Type</TT>, <A HREF="Reference-Manual004.html#@default100">2.5.10</A>
</LI><LI CLASS="li-indexenv"><TT>Print Modules</TT>, <A HREF="Reference-Manual008.html#@default368">6.4.2</A>
</LI><LI CLASS="li-indexenv"><TT>Print Section</TT>, <A HREF="Reference-Manual008.html#@default343">2</A>
</LI><LI CLASS="li-indexenv"><TT>Print Table Printing If</TT>, <A HREF="Reference-Manual004.html#@default86">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Print Table Printing Let</TT>, <A HREF="Reference-Manual004.html#@default82">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Print Term</TT>, <A HREF="Reference-Manual008.html#@default339">1</A>
</LI><LI CLASS="li-indexenv"><TT>Print Universes</TT>, <A HREF="Reference-Manual004.html#@default127">2.10</A>
</LI><LI CLASS="li-indexenv"><TT>Print XML</TT>, <A HREF="Reference-Manual016.html#@default721">13.5.5</A>
</LI><LI CLASS="li-indexenv">Program, <A HREF="Reference-Manual024.html#@default778">19</A>
</LI><LI CLASS="li-indexenv"><TT>Program Definition</TT>, <A HREF="Reference-Manual024.html#@default779">19.1.1</A>
</LI><LI CLASS="li-indexenv"><TT>Program Fixpoint</TT>, <A HREF="Reference-Manual024.html#@default780">19.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>Program Lemma</TT>, <A HREF="Reference-Manual024.html#@default781">19.1.3</A>
</LI><LI CLASS="li-indexenv">Programming, <A HREF="Reference-Manual005.html#@default165">3.1.3</A>
</LI><LI CLASS="li-indexenv">Prompt, <A HREF="Reference-Manual009.html#@default404">7</A>
</LI><LI CLASS="li-indexenv"><TT>Proof</TT>, <A HREF="Reference-Manual003.html#@default58">1.3.5</A>, <A HREF="Reference-Manual009.html#@default418">7.1.5</A>
</LI><LI CLASS="li-indexenv">Proof editing, <A HREF="Reference-Manual009.html#@default403">7</A>
</LI><LI CLASS="li-indexenv">Proof General, <A HREF="Reference-Manual016.html#@default726">13.7.2</A>
</LI><LI CLASS="li-indexenv">Proof rendering, <A HREF="Reference-Manual016.html#@default720">13.5</A>
</LI><LI CLASS="li-indexenv">Proof term, <A HREF="Reference-Manual009.html#@default406">7</A>
</LI><LI CLASS="li-indexenv"><TT>Proof with</TT>, <A HREF="Reference-Manual010.html#@default610">8.13.6</A>
</LI><LI CLASS="li-indexenv"><FONT COLOR=purple>Prop</FONT>, <A HREF="Reference-Manual003.html#@default15">1.2.5</A>, <A HREF="Reference-Manual006.html#@default295">4.1.1</A>
</LI><LI CLASS="li-indexenv"><TT>Proposition</TT>, <A HREF="Reference-Manual003.html#@default56">1</A>
</LI><LI CLASS="li-indexenv"><TT>Pwd</TT>, <A HREF="Reference-Manual008.html#@default372">6.5.1</A>
</LI><LI CLASS="li-indexenv"><TT>pair</TT>, <A HREF="Reference-Manual005.html#@default187">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>pairT</TT>, <A HREF="Reference-Manual005.html#@default258">3.1.7</A>
</LI><LI CLASS="li-indexenv"><TT>pattern</TT>, <A HREF="Reference-Manual010.html#@default500">8.5.7</A>
</LI><LI CLASS="li-indexenv">p<SPAN STYLE="font-variant:small-caps">CIC</SPAN>, <A HREF="Reference-Manual006.html#@default289">4</A>
</LI><LI CLASS="li-indexenv"><TT>plus</TT>, <A HREF="Reference-Manual005.html#@default231">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>plus_n_O</TT>, <A HREF="Reference-Manual005.html#@default232">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>plus_n_Sm</TT>, <A HREF="Reference-Manual005.html#@default233">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>pose</TT>, <A HREF="Reference-Manual010.html#@default468">8.3.7</A>
</LI><LI CLASS="li-indexenv"><TT>pred</TT>, <A HREF="Reference-Manual005.html#@default224">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>pred_Sn</TT>, <A HREF="Reference-Manual005.html#@default225">3.1.5</A>
</LI><LI CLASS="li-indexenv"><TT>prod</TT>, <A HREF="Reference-Manual005.html#@default184">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>prodT</TT>, <A HREF="Reference-Manual005.html#@default257">3.1.7</A>
</LI><LI CLASS="li-indexenv">products, <A HREF="Reference-Manual003.html#@default22">1.2.8</A>
</LI><LI CLASS="li-indexenv"><TT>progress</TT>, <A HREF="Reference-Manual011.html#@default627">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>proj1</TT>, <A HREF="Reference-Manual005.html#@default136">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>proj2</TT>, <A HREF="Reference-Manual005.html#@default137">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>projS1</TT>, <A HREF="Reference-Manual005.html#@default200">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>projS2</TT>, <A HREF="Reference-Manual005.html#@default201">3.1.4</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>Qed</TT>, <A HREF="Reference-Manual003.html#@default59">1.3.5</A>, <A HREF="Reference-Manual009.html#@default408">7.1.2</A>
</LI><LI CLASS="li-indexenv">Qualified identifiers, <A HREF="Reference-Manual004.html#@default104">2.6.2</A>
</LI><LI CLASS="li-indexenv">Quantifiers, <A HREF="Reference-Manual005.html#@default143">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>Quit</TT>, <A HREF="Reference-Manual008.html#@default388">6.7.1</A>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>qualid</FONT></I>, <A HREF="Reference-Manual004.html#@default115">2.7.7</A>
</LI><LI CLASS="li-indexenv"><TT>quote</TT>, <A HREF="Reference-Manual010.html#@default574">8.10.4</A>, <A HREF="Reference-Manual012.html#@default680">10.7</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>Record</TT>, <A HREF="Reference-Manual004.html#@default65">2.1</A>
</LI><LI CLASS="li-indexenv">Recursion, <A HREF="Reference-Manual005.html#@default246">3.1.6</A>
</LI><LI CLASS="li-indexenv">Recursive arguments, <A HREF="Reference-Manual006.html#@default335">4.5.5</A>
</LI><LI CLASS="li-indexenv"><TT>Recursive Extraction</TT>, <A HREF="Reference-Manual023.html#@default764">18.1</A>
</LI><LI CLASS="li-indexenv"><TT>Recursive Extraction Module</TT>, <A HREF="Reference-Manual023.html#@default766">18.1</A>
</LI><LI CLASS="li-indexenv"><TT>Remark</TT>, <A HREF="Reference-Manual003.html#@default54">1.3.5</A>, <A HREF="Reference-Manual009.html#@default414">2</A>
</LI><LI CLASS="li-indexenv"><TT>Remove LoadPath</TT>, <A HREF="Reference-Manual008.html#@default376">6.5.5</A>
</LI><LI CLASS="li-indexenv"><TT>Remove Printing If </TT><I><FONT COLOR=maroon>ident</FONT></I>, <A HREF="Reference-Manual004.html#@default84">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Remove Printing Let </TT><I><FONT COLOR=maroon>ident</FONT></I>, <A HREF="Reference-Manual004.html#@default80">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Require</TT>, <A HREF="Reference-Manual008.html#@default365">6.4.1</A>
</LI><LI CLASS="li-indexenv"><TT>Require Export</TT>, <A HREF="Reference-Manual008.html#@default366">1</A>
</LI><LI CLASS="li-indexenv"><TT>ReservedNotation</TT>, <A HREF="Reference-Manual013.html#@default687">11.1.7</A>
</LI><LI CLASS="li-indexenv"><TT>Reset</TT>, <A HREF="Reference-Manual008.html#@default383">6.6.1</A>
</LI><LI CLASS="li-indexenv"><TT>Reset Extraction Inline</TT>, <A HREF="Reference-Manual023.html#@default775">18.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>Reset Initial</TT>, <A HREF="Reference-Manual008.html#@default386">2</A>
</LI><LI CLASS="li-indexenv">Resource file, <A HREF="Reference-Manual015.html#@default709">12.3</A>
</LI><LI CLASS="li-indexenv"><TT>Restart</TT>, <A HREF="Reference-Manual009.html#@default425">7.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Restore State</TT>, <A HREF="Reference-Manual008.html#@default385">6.6.3</A>
</LI><LI CLASS="li-indexenv"><TT>Resume</TT>, <A HREF="Reference-Manual009.html#@default421">7.1.8</A>
</LI><LI CLASS="li-indexenv"><TT>red</TT>, <A HREF="Reference-Manual010.html#@default493">8.5.2</A>
</LI><LI CLASS="li-indexenv"><TT>refine</TT>, <A HREF="Reference-Manual010.html#@default444">8.2.2</A>, <A HREF="Reference-Manual012.html#@default674">10.1</A>
</LI><LI CLASS="li-indexenv"><TT>refl_equal</TT>, <A HREF="Reference-Manual005.html#@default153">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>refl_identity</TT>, <A HREF="Reference-Manual005.html#@default178">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>reflexivity</TT>, <A HREF="Reference-Manual010.html#@default530">8.8.4</A>
</LI><LI CLASS="li-indexenv"><TT>rename</TT>, <A HREF="Reference-Manual010.html#@default453">8.3.4</A>
</LI><LI CLASS="li-indexenv"><TT>repeat</TT>, <A HREF="Reference-Manual011.html#@default623">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>replace &#X2026; with</TT>, <A HREF="Reference-Manual010.html#@default529">8.8.3</A>
</LI><LI CLASS="li-indexenv"><TT>rev</TT>, <A HREF="Reference-Manual005.html#@default281">3.2.5</A>
</LI><LI CLASS="li-indexenv"><TT>rewrite</TT>, <A HREF="Reference-Manual010.html#@default522">8.8.1</A>
</LI><LI CLASS="li-indexenv"><TT>rewrite -&gt;</TT>, <A HREF="Reference-Manual010.html#@default523">1</A>
</LI><LI CLASS="li-indexenv"><TT>rewrite -&gt; &#X2026; in</TT>, <A HREF="Reference-Manual010.html#@default526">4</A>
</LI><LI CLASS="li-indexenv"><TT>rewrite &lt;-</TT>, <A HREF="Reference-Manual010.html#@default524">2</A>
</LI><LI CLASS="li-indexenv"><TT>rewrite &lt;- &#X2026; in</TT>, <A HREF="Reference-Manual010.html#@default527">5</A>
</LI><LI CLASS="li-indexenv"><TT>rewrite &#X2026; in</TT>, <A HREF="Reference-Manual010.html#@default525">3</A>
</LI><LI CLASS="li-indexenv"><TT>right</TT>, <A HREF="Reference-Manual005.html#@default206">3.1.4</A>, <A HREF="Reference-Manual010.html#@default506">5</A>
</LI><LI CLASS="li-indexenv"><TT>ring</TT>, <A HREF="Reference-Manual010.html#@default591">8.12.9</A>, <A HREF="Reference-Manual025.html#@default782">20</A>, <A HREF="Reference-Manual025.html#@default783">20.4</A>
</LI><LI CLASS="li-indexenv"><TT>ring_simplify</TT>, <A HREF="Reference-Manual010.html#@default592">8.12.9</A>, <A HREF="Reference-Manual025.html#@default784">20.4</A>
</LI><LI CLASS="li-indexenv"><TT>rtauto</TT>, <A HREF="Reference-Manual010.html#@default583">8.12.5</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>S</TT>, <A HREF="Reference-Manual005.html#@default173">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>Save</TT>, <A HREF="Reference-Manual003.html#@default61">1.3.5</A>, <A HREF="Reference-Manual009.html#@default410">2</A>
</LI><LI CLASS="li-indexenv"><TT>Scheme</TT>, <A HREF="Reference-Manual010.html#@default612">8.14</A>, <A HREF="Reference-Manual012.html#@default676">10.3</A>
</LI><LI CLASS="li-indexenv">Script file, <A HREF="Reference-Manual008.html#@default361">6.3</A>
</LI><LI CLASS="li-indexenv"><TT>Search</TT>, <A HREF="Reference-Manual008.html#@default349">6.2.6</A>
</LI><LI CLASS="li-indexenv"><TT>SearchAbout</TT>, <A HREF="Reference-Manual008.html#@default350">6.2.7</A>
</LI><LI CLASS="li-indexenv"><TT>SearchPattern</TT>, <A HREF="Reference-Manual008.html#@default351">6.2.8</A>
</LI><LI CLASS="li-indexenv"><TT>SearchPattern &#X2026; inside
&#X2026;</TT>, <A HREF="Reference-Manual008.html#@default352">1</A>
</LI><LI CLASS="li-indexenv"><TT>SearchPattern &#X2026; outside &#X2026;</TT>, <A HREF="Reference-Manual008.html#@default353">2</A>
</LI><LI CLASS="li-indexenv"><TT>SearchRewrite</TT>, <A HREF="Reference-Manual008.html#@default354">6.2.9</A>
</LI><LI CLASS="li-indexenv"><TT>Section</TT>, <A HREF="Reference-Manual004.html#@default89">2.4.1</A>
</LI><LI CLASS="li-indexenv">Sections, <A HREF="Reference-Manual004.html#@default88">2.4</A>
</LI><LI CLASS="li-indexenv"><FONT COLOR=purple>Set</FONT>, <A HREF="Reference-Manual003.html#@default14">1.2.5</A>, <A HREF="Reference-Manual006.html#@default296">4.1.1</A>
</LI><LI CLASS="li-indexenv"><TT>Set Contextual Implicit</TT>, <A HREF="Reference-Manual004.html#@default112">2.7.6</A>
</LI><LI CLASS="li-indexenv"><TT>Set Extraction AutoInline</TT>, <A HREF="Reference-Manual023.html#@default770">18.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>Set Extraction Optimize</TT>, <A HREF="Reference-Manual023.html#@default768">18.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>Set Firstorder Depth</TT>, <A HREF="Reference-Manual010.html#@default588">8.12.6</A>
</LI><LI CLASS="li-indexenv"><TT>Set Hyps Limit</TT>, <A HREF="Reference-Manual009.html#@default436">7.3.2</A>
</LI><LI CLASS="li-indexenv"><TT>Set Implicit Arguments</TT>, <A HREF="Reference-Manual004.html#@default108">2.7.4</A>
</LI><LI CLASS="li-indexenv"><TT>Set Ltac Debug</TT>, <A HREF="Reference-Manual011.html#@default671">9.4</A>
</LI><LI CLASS="li-indexenv"><TT>Set Printing All</TT>, <A HREF="Reference-Manual004.html#@default123">2.9</A>
</LI><LI CLASS="li-indexenv"><TT>Set Printing Coercion</TT>, <A HREF="Reference-Manual021.html#@default756">16.8.2</A>
</LI><LI CLASS="li-indexenv"><TT>Set Printing Coercions</TT>, <A HREF="Reference-Manual021.html#@default754">16.8.1</A>
</LI><LI CLASS="li-indexenv"><TT>Set Printing Depth</TT>, <A HREF="Reference-Manual008.html#@default397">6.8.6</A>
</LI><LI CLASS="li-indexenv"><TT>Set Printing Implicit</TT>, <A HREF="Reference-Manual004.html#@default117">2.7.9</A>
</LI><LI CLASS="li-indexenv"><TT>Set Printing Matching</TT>, <A HREF="Reference-Manual004.html#@default70">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Set Printing Notations</TT>, <A HREF="Reference-Manual013.html#@default691">11.1.9</A>
</LI><LI CLASS="li-indexenv"><TT>Set Printing Synth</TT>, <A HREF="Reference-Manual004.html#@default76">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Set Printing Universes</TT>, <A HREF="Reference-Manual004.html#@default125">2.10</A>
</LI><LI CLASS="li-indexenv"><TT>Set Printing Width</TT>, <A HREF="Reference-Manual008.html#@default394">6.8.3</A>
</LI><LI CLASS="li-indexenv"><TT>Set Printing Wildcard</TT>, <A HREF="Reference-Manual004.html#@default73">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Set Strict Implicit</TT>, <A HREF="Reference-Manual004.html#@default110">2.7.5</A>
</LI><LI CLASS="li-indexenv"><TT>Set Undo</TT>, <A HREF="Reference-Manual009.html#@default423">7.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>Set Virtual Machine</TT>, <A HREF="Reference-Manual008.html#@default400">6.9.1</A>
</LI><LI CLASS="li-indexenv"><TT>Show</TT>, <A HREF="Reference-Manual009.html#@default428">7.3.1</A>
</LI><LI CLASS="li-indexenv"><TT>Show Conjectures</TT>, <A HREF="Reference-Manual009.html#@default433">7</A>
</LI><LI CLASS="li-indexenv"><TT>Show Implicits</TT>, <A HREF="Reference-Manual009.html#@default429">2</A>
</LI><LI CLASS="li-indexenv"><TT>Show Intro</TT>, <A HREF="Reference-Manual009.html#@default434">8</A>
</LI><LI CLASS="li-indexenv"><TT>Show Intros</TT>, <A HREF="Reference-Manual009.html#@default435">9</A>
</LI><LI CLASS="li-indexenv"><TT>Show Proof</TT>, <A HREF="Reference-Manual009.html#@default432">6</A>
</LI><LI CLASS="li-indexenv"><TT>Show Script</TT>, <A HREF="Reference-Manual009.html#@default430">4</A>
</LI><LI CLASS="li-indexenv"><TT>Show Tree</TT>, <A HREF="Reference-Manual009.html#@default431">5</A>
</LI><LI CLASS="li-indexenv"><TT>Show XML Proof</TT>, <A HREF="Reference-Manual016.html#@default722">13.5.5</A>
</LI><LI CLASS="li-indexenv">Silent mode, <A HREF="Reference-Manual008.html#@default392">6.8.1</A>
</LI><LI CLASS="li-indexenv"><TT>Some</TT>, <A HREF="Reference-Manual005.html#@default175">3.1.3</A>
</LI><LI CLASS="li-indexenv">Sort-polymorphism of inductive families, <A HREF="Reference-Manual006.html#@default326">4.5.3</A>
</LI><LI CLASS="li-indexenv">Sorts, <A HREF="Reference-Manual003.html#@default12">1.2.5</A>, <A HREF="Reference-Manual003.html#@default16">1.2.5</A>, <A HREF="Reference-Manual006.html#@default293">4.1.1</A>
</LI><LI CLASS="li-indexenv"><TT>Structure</TT>, <A HREF="Reference-Manual021.html#@default759">16.9</A>
</LI><LI CLASS="li-indexenv"><TT>SubClass</TT>, <A HREF="Reference-Manual021.html#@default749">2</A>
</LI><LI CLASS="li-indexenv">Substitution, <A HREF="Reference-Manual006.html#@default298">4.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>Suspend</TT>, <A HREF="Reference-Manual009.html#@default420">7.1.7</A>
</LI><LI CLASS="li-indexenv">Syntactic Definition, <A HREF="Reference-Manual013.html#@default704">11.3</A>
</LI><LI CLASS="li-indexenv"><TT>set</TT>, <A HREF="Reference-Manual010.html#@default467">8.3.7</A>
</LI><LI CLASS="li-indexenv"><TT>setoid_reflexivity</TT>, <A HREF="Reference-Manual026.html#@default803">21.7</A>
</LI><LI CLASS="li-indexenv"><TT>setoid_replace</TT>, <A HREF="Reference-Manual026.html#@default799">21</A>, <A HREF="Reference-Manual026.html#@default807">21.7</A>
</LI><LI CLASS="li-indexenv"><TT>setoid_rewrite</TT>, <A HREF="Reference-Manual026.html#@default802">21.5</A>, <A HREF="Reference-Manual026.html#@default806">21.7</A>
</LI><LI CLASS="li-indexenv"><TT>setoid_symmetry</TT>, <A HREF="Reference-Manual026.html#@default804">21.7</A>
</LI><LI CLASS="li-indexenv"><TT>setoid_transitivity</TT>, <A HREF="Reference-Manual026.html#@default805">21.7</A>
</LI><LI CLASS="li-indexenv"><TT>sig</TT>, <A HREF="Reference-Manual005.html#@default192">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>sig2</TT>, <A HREF="Reference-Manual005.html#@default194">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>sigS</TT>, <A HREF="Reference-Manual005.html#@default198">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>sigS2</TT>, <A HREF="Reference-Manual005.html#@default202">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>simpl</TT>, <A HREF="Reference-Manual010.html#@default495">8.5.4</A>
</LI><LI CLASS="li-indexenv"><TT>simpl &#X2026; in</TT>, <A HREF="Reference-Manual010.html#@default496">8.5.4</A>
</LI><LI CLASS="li-indexenv"><TT>simple destruct</TT>, <A HREF="Reference-Manual010.html#@default515">7</A>
</LI><LI CLASS="li-indexenv"><TT>simple induction</TT>, <A HREF="Reference-Manual010.html#@default511">11</A>
</LI><LI CLASS="li-indexenv"><TT>simple inversion</TT>, <A HREF="Reference-Manual010.html#@default565">18</A>
</LI><LI CLASS="li-indexenv"><TT>simple inversion &#X2026; as</TT>, <A HREF="Reference-Manual010.html#@default566">19</A>
</LI><LI CLASS="li-indexenv"><TT>simplify_eq</TT>, <A HREF="Reference-Manual010.html#@default546">8.9.5</A>
</LI><LI CLASS="li-indexenv"><TT>snd</TT>, <A HREF="Reference-Manual005.html#@default189">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>solve</TT>, <A HREF="Reference-Manual011.html#@default632">9.2</A>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>sort</FONT></I>, <A HREF="Reference-Manual003.html#@default10">1.1</A>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>specif</FONT></I>, <A HREF="Reference-Manual003.html#@default18">1.2.5</A>
</LI><LI CLASS="li-indexenv"><TT>split</TT>, <A HREF="Reference-Manual010.html#@default503">3</A>
</LI><LI CLASS="li-indexenv"><TT>split_Rabs</TT>, <A HREF="Reference-Manual005.html#@default274">3.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>split_Rmult</TT>, <A HREF="Reference-Manual005.html#@default275">3.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>stepl</TT>, <A HREF="Reference-Manual010.html#@default535">8.8.8</A>
</LI><LI CLASS="li-indexenv"><TT>stepr</TT>, <A HREF="Reference-Manual010.html#@default537">8.8.8</A>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>string</FONT></I>, <A HREF="Reference-Manual003.html#@default7">1.1</A>
</LI><LI CLASS="li-indexenv">subgoal, <A HREF="Reference-Manual010.html#@default440">8</A>
</LI><LI CLASS="li-indexenv"><TT>subst</TT>, <A HREF="Reference-Manual010.html#@default534">8.8.7</A>
</LI><LI CLASS="li-indexenv"><TT>sum</TT>, <A HREF="Reference-Manual005.html#@default179">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>sumbool</TT>, <A HREF="Reference-Manual005.html#@default204">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>sumor</TT>, <A HREF="Reference-Manual005.html#@default208">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>sym_eq</TT>, <A HREF="Reference-Manual005.html#@default155">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>sym_not_eq</TT>, <A HREF="Reference-Manual005.html#@default158">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>symmetry</TT>, <A HREF="Reference-Manual010.html#@default531">8.8.5</A>
</LI><LI CLASS="li-indexenv"><TT>symmetry in</TT>, <A HREF="Reference-Manual010.html#@default532">8.8.5</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>Tactic Definition</TT>, <A HREF="Reference-Manual010.html#@default615">8.16</A>
</LI><LI CLASS="li-indexenv">Tacticals, <A HREF="Reference-Manual011.html#@default616">9.2</A>
<UL CLASS="indexenv"><LI CLASS="li-indexenv">
<I><FONT COLOR=maroon>tactic</FONT></I><SUB><TT>1</TT></SUB><TT>;</TT><I><FONT COLOR=maroon>tactic</FONT></I><SUB><TT>2</TT></SUB>, <A HREF="Reference-Manual011.html#@default618">9.2</A>
</LI><LI CLASS="li-indexenv">; [ ,  ]<A HREF="Reference-Manual011.html#@default620">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>abstract</TT>, <A HREF="Reference-Manual011.html#@default667">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>do</TT>, <A HREF="Reference-Manual011.html#@default622">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>fail</TT>, <A HREF="Reference-Manual011.html#@default637">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>first</TT>, <A HREF="Reference-Manual011.html#@default631">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>idtac</TT>, <A HREF="Reference-Manual011.html#@default635">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>info</TT>, <A HREF="Reference-Manual011.html#@default665">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>&#X2223;&#X2223;</TT>, <A HREF="Reference-Manual011.html#@default629">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>repeat</TT>, <A HREF="Reference-Manual011.html#@default624">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>solve</TT>, <A HREF="Reference-Manual011.html#@default633">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>try</TT>, <A HREF="Reference-Manual011.html#@default626">9.2</A>
</LI></UL>
</LI><LI CLASS="li-indexenv">Tactics, <A HREF="Reference-Manual010.html#@default438">8</A>
</LI><LI CLASS="li-indexenv">Terms, <A HREF="Reference-Manual003.html#@default8">1.2</A>
</LI><LI CLASS="li-indexenv"><TT>Test Ltac Debug</TT>, <A HREF="Reference-Manual011.html#@default673">9.4</A>
</LI><LI CLASS="li-indexenv"><TT>Test Printing Depth</TT>, <A HREF="Reference-Manual008.html#@default399">6.8.8</A>
</LI><LI CLASS="li-indexenv"><TT>Test Printing If </TT><I><FONT COLOR=maroon>ident</FONT></I>, <A HREF="Reference-Manual004.html#@default85">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Test Printing Let </TT><I><FONT COLOR=maroon>ident</FONT></I>, <A HREF="Reference-Manual004.html#@default81">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Test Printing Matching</TT>, <A HREF="Reference-Manual004.html#@default72">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Test Printing Synth</TT>, <A HREF="Reference-Manual004.html#@default78">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Test Printing Width</TT>, <A HREF="Reference-Manual008.html#@default396">6.8.5</A>
</LI><LI CLASS="li-indexenv"><TT>Test Printing Wildcard</TT>, <A HREF="Reference-Manual004.html#@default75">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Test Virtual Machine</TT>, <A HREF="Reference-Manual008.html#@default402">6.9.3</A>
</LI><LI CLASS="li-indexenv"><TT>Theorem</TT>, <A HREF="Reference-Manual003.html#@default52">1.3.5</A>, <A HREF="Reference-Manual009.html#@default412">7.1.4</A>
</LI><LI CLASS="li-indexenv">Theories, <A HREF="Reference-Manual005.html#@default128">3</A>
</LI><LI CLASS="li-indexenv"><TT>Time</TT>, <A HREF="Reference-Manual008.html#@default390">6.7.3</A>
</LI><LI CLASS="li-indexenv"><TT>Transparent</TT>, <A HREF="Reference-Manual008.html#@default348">6.2.5</A>
</LI><LI CLASS="li-indexenv"><TT>True</TT>, <A HREF="Reference-Manual005.html#@default130">3.1.2</A>
</LI><LI CLASS="li-indexenv"><FONT COLOR=purple>Type</FONT>, <A HREF="Reference-Manual003.html#@default13">1.2.5</A>, <A HREF="Reference-Manual006.html#@default294">4.1.1</A>
</LI><LI CLASS="li-indexenv">Type of constructor, <A HREF="Reference-Manual006.html#@default325">4.5.3</A>
</LI><LI CLASS="li-indexenv">Typing rules, <A HREF="Reference-Manual006.html#@default301">4.2</A>, <A HREF="Reference-Manual010.html#@default446">8.3</A>
<UL CLASS="indexenv"><LI CLASS="li-indexenv">
App, <A HREF="Reference-Manual006.html#@default307">4.2</A>, <A HREF="Reference-Manual010.html#@default471">3</A>
</LI><LI CLASS="li-indexenv">Ax, <A HREF="Reference-Manual006.html#@default302">4.2</A>
</LI><LI CLASS="li-indexenv">Const, <A HREF="Reference-Manual006.html#@default304">4.2</A>
</LI><LI CLASS="li-indexenv">Conv, <A HREF="Reference-Manual006.html#@default318">4.3</A>, <A HREF="Reference-Manual010.html#@default457">8.3.5</A>, <A HREF="Reference-Manual010.html#@default478">8.3.11</A>
</LI><LI CLASS="li-indexenv">Fix, <A HREF="Reference-Manual006.html#@default334">4.5.5</A>
</LI><LI CLASS="li-indexenv">Lam, <A HREF="Reference-Manual006.html#@default306">4.2</A>, <A HREF="Reference-Manual010.html#@default455">8.3.5</A>
</LI><LI CLASS="li-indexenv">Let, <A HREF="Reference-Manual006.html#@default308">4.2</A>, <A HREF="Reference-Manual010.html#@default456">8.3.5</A>
</LI><LI CLASS="li-indexenv">match, <A HREF="Reference-Manual006.html#@default331">4.5.4</A>
</LI><LI CLASS="li-indexenv">Prod, <A HREF="Reference-Manual006.html#@default305">4.2</A>
</LI><LI CLASS="li-indexenv">Prod (impredicative Set), <A HREF="Reference-Manual006.html#@default337">4.7</A>
</LI><LI CLASS="li-indexenv">Var, <A HREF="Reference-Manual006.html#@default303">4.2</A>, <A HREF="Reference-Manual010.html#@default448">8.3.1</A>
</LI></UL>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>tactic</FONT></I>, <A HREF="Reference-Manual010.html#@default441">8.1</A>
</LI><LI CLASS="li-indexenv">tactic macros, <A HREF="Reference-Manual010.html#@default614">8.16</A>
</LI><LI CLASS="li-indexenv"><TT>tail</TT>, <A HREF="Reference-Manual005.html#@default279">3.2.5</A>
</LI><LI CLASS="li-indexenv"><TT>tauto</TT>, <A HREF="Reference-Manual010.html#@default581">8.12.3</A>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>term</FONT></I>, <A HREF="Reference-Manual003.html#@default9">1.1</A>
</LI><LI CLASS="li-indexenv"><TT>trans_eq</TT>, <A HREF="Reference-Manual005.html#@default156">3.1.2</A>
</LI><LI CLASS="li-indexenv"><TT>transitivity</TT>, <A HREF="Reference-Manual010.html#@default533">8.8.6</A>
</LI><LI CLASS="li-indexenv"><TT>trivial</TT>, <A HREF="Reference-Manual010.html#@default579">5</A>
</LI><LI CLASS="li-indexenv"><TT>true</TT>, <A HREF="Reference-Manual005.html#@default169">3.1.3</A>
</LI><LI CLASS="li-indexenv"><TT>try</TT>, <A HREF="Reference-Manual011.html#@default625">9.2</A>
</LI><LI CLASS="li-indexenv"><TT>tt</TT>, <A HREF="Reference-Manual005.html#@default167">3.1.3</A>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>type</FONT></I>, <A HREF="Reference-Manual003.html#@default11">1.2.2</A>, <A HREF="Reference-Manual003.html#@default19">1.2.5</A>
</LI><LI CLASS="li-indexenv">type of<UL CLASS="indexenv"><LI CLASS="li-indexenv">
in Ltac, <A HREF="Reference-Manual011.html#@default663">9.2</A>
</LI></UL>
</LI><LI CLASS="li-indexenv">type_scope, <A HREF="Reference-Manual013.html#@default701">11.2.3</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>Undo</TT>, <A HREF="Reference-Manual009.html#@default422">7.2.1</A>
</LI><LI CLASS="li-indexenv"><TT>Unfocus</TT>, <A HREF="Reference-Manual009.html#@default427">7.2.6</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Contextual Implicit</TT>, <A HREF="Reference-Manual004.html#@default113">2.7.6</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Extraction AutoInline</TT>, <A HREF="Reference-Manual023.html#@default771">18.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Extraction Optimize</TT>, <A HREF="Reference-Manual023.html#@default769">18.2.2</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Hyps Limit</TT>, <A HREF="Reference-Manual009.html#@default437">7.3.3</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Implicit Arguments</TT>, <A HREF="Reference-Manual004.html#@default109">2.7.4</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Ltac Debug</TT>, <A HREF="Reference-Manual011.html#@default672">9.4</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Printing All</TT>, <A HREF="Reference-Manual004.html#@default124">2.9</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Printing Coercion</TT>, <A HREF="Reference-Manual021.html#@default757">16.8.2</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Printing Coercions</TT>, <A HREF="Reference-Manual021.html#@default755">16.8.1</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Printing Depth</TT>, <A HREF="Reference-Manual008.html#@default398">6.8.7</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Printing Implicit</TT>, <A HREF="Reference-Manual004.html#@default118">2.7.9</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Printing Matching</TT>, <A HREF="Reference-Manual004.html#@default71">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Printing Notations</TT>, <A HREF="Reference-Manual013.html#@default692">11.1.9</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Printing Synth</TT>, <A HREF="Reference-Manual004.html#@default77">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Printing Universes</TT>, <A HREF="Reference-Manual004.html#@default126">2.10</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Printing Width</TT>, <A HREF="Reference-Manual008.html#@default395">6.8.4</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Printing Wildcard</TT>, <A HREF="Reference-Manual004.html#@default74">2.2.4</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Strict Implicit</TT>, <A HREF="Reference-Manual004.html#@default111">2.7.5</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Undo</TT>, <A HREF="Reference-Manual009.html#@default424">7.2.3</A>
</LI><LI CLASS="li-indexenv"><TT>Unset Virtual Machine</TT>, <A HREF="Reference-Manual008.html#@default401">6.9.2</A>
</LI><LI CLASS="li-indexenv"><TT>unfold</TT>, <A HREF="Reference-Manual010.html#@default497">8.5.5</A>
</LI><LI CLASS="li-indexenv"><TT>unfold &#X2026; in</TT>, <A HREF="Reference-Manual010.html#@default498">1</A>
</LI><LI CLASS="li-indexenv"><TT>unit</TT>, <A HREF="Reference-Manual005.html#@default166">3.1.3</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv"><TT>Variable</TT>, <A HREF="Reference-Manual003.html#@default35">1.3.1</A>
</LI><LI CLASS="li-indexenv"><TT>Variable </TT>(and coercions), <A HREF="Reference-Manual021.html#@default742">5</A>
</LI><LI CLASS="li-indexenv"><TT>Variables</TT>, <A HREF="Reference-Manual003.html#@default36">1.3.1</A>
</LI><LI CLASS="li-indexenv"><TT>value</TT>, <A HREF="Reference-Manual005.html#@default216">3.1.4</A>
</LI><LI CLASS="li-indexenv"><TT>vm_compute</TT>, <A HREF="Reference-Manual010.html#@default490">8.5.1</A>, <A HREF="Reference-Manual010.html#@default492">2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Well founded induction, <A HREF="Reference-Manual005.html#@default247">3.1.6</A>
</LI><LI CLASS="li-indexenv">Well foundedness, <A HREF="Reference-Manual005.html#@default245">3.1.6</A>
</LI><LI CLASS="li-indexenv"><TT>Whelp Elim</TT>, <A HREF="Reference-Manual008.html#@default359">6.2.11</A>
</LI><LI CLASS="li-indexenv"><TT>Whelp Hint</TT>, <A HREF="Reference-Manual008.html#@default360">6.2.11</A>
</LI><LI CLASS="li-indexenv"><TT>Whelp Instance</TT>, <A HREF="Reference-Manual008.html#@default358">6.2.11</A>
</LI><LI CLASS="li-indexenv"><TT>Whelp Locate</TT>, <A HREF="Reference-Manual008.html#@default356">6.2.11</A>
</LI><LI CLASS="li-indexenv"><TT>Whelp Match</TT>, <A HREF="Reference-Manual008.html#@default357">6.2.11</A>
</LI><LI CLASS="li-indexenv"><TT>Write State</TT>, <A HREF="Reference-Manual008.html#@default387">6.6.4</A>
</LI><LI CLASS="li-indexenv"><TT>well_founded</TT>, <A HREF="Reference-Manual005.html#@default251">3.1.6</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">XML exportation, <A HREF="Reference-Manual016.html#@default719">13.5</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">&#X3B6;-reduction, <A HREF="Reference-Manual006.html#@default313">4.3</A>, <A HREF="Reference-Manual006.html#@default317">4.3</A>
</LI></UL></TD></TR>
</TABLE><HR>
<A HREF="biblio.html"><IMG SRC="previous_motif.gif" ALT="Previous"></A>
<A HREF="toc.html"><IMG SRC="contents_motif.gif" ALT="Up"></A>
<A HREF="tactic-index.html"><IMG SRC="next_motif.gif" ALT="Next"></A>
</BODY>
</HTML>
